(DEFPROP ALLFNS
 (NIL OCCUR COM1 COM2 COM3 COM4 COM5 COM6 COMMON FIX SUBSTT)
VALUE)

(DEFPROP OCCUR
 (LAMBDA (E U) (OR (EQUAL E U) (AND (NOT (ATOM U)) (OR (OCCUR E (CAR U)) (OCCUR E (CDR U))))))
EXPR)

(DEFPROP COM1
 (LAMBDA (E) (COND ((ATOM E) NIL) (T (COM2 (CDR E)))))
EXPR)

(DEFPROP COM2
 (LAMBDA(U)
  (COND ((NULL U) NIL) (T ((LAMBDA (Z) (COND ((NULL Z) (COM2 (CDR U))) (T Z))) (COM3 (CAR U) (CDR U))))))
EXPR)

(DEFPROP COM3
 (LAMBDA (E U) (COND ((ATOM E) NIL) ((OCCUR E U) E) (T (COM4 (CDR E) U))))
EXPR)

(DEFPROP COM4
 (LAMBDA(V U)
  (COND ((NULL V) NIL) (T ((LAMBDA (Z) (COND ((NULL Z) (COM4 (CDR V) U)) (T Z))) (COM3 (CAR V) U)))))
EXPR)

(DEFPROP COM5
 (LAMBDA(E)
  ((LAMBDA (Z) (COND ((NULL Z) NIL) (T ((LAMBDA (W) (COND ((NULL W) Z) (T (COM5 W)))) (COM1 Z))))) (COM1 E)))
EXPR)

(DEFPROP COM6
 (LAMBDA (E1 E) ((LAMBDA (Z) (COND ((NULL Z) E1) (T (COM6 Z E)))) (COM3 E1 (SUBSTT (GENSYM) E1 E))))
EXPR)

(DEFPROP COMMON
 (LAMBDA (E) ((LAMBDA (Z) (COND ((NULL Z) NIL) (T (COM6 Z E)))) (COM5 E)))
EXPR)

(DEFPROP SUBSTT
 (LAMBDA (X Y Z) (COND ((EQUAL Y Z) X) ((ATOM Z) Z) (T (CONS (SUBSTT X Y (CAR Z)) (SUBSTT X Y (CDR Z))))))
EXPR)